es:ES, i, x:Id, L:Knd List. @i: only members of L read x  Prop 

latex

Definitions	ES, t  T, Id, Knd, type List, x:A. B(x), es-independent(es;i;k;x), (x  l), A, x:AB(x), Prop, P  Q, hasloc(k;i), b, Type, @i: only members of L read x
Lemmas	assert wf, hasloc wf, not wf, l member wf, es-independent wf, Knd wf, Id wf, event system wf